Kernel-check the Section 9 matching-restriction product bound - #34

Summary

This PR translates the finite combinatorial core of PR #30 into Lean.

For a finite even bipartite edge set and an exposed matching M, deleting M is injective. Consequently the weighted even-family sum is bounded directly by the full subset product on the cells outside M, without a cycle decomposition.

Files

• 625/formalization/Erdos625/Section9MatchingRestrictionProduct.lean
• 625/formalization/MATCHING_RESTRICTION_PRODUCT_AUDIT.md
• .github/workflows/erdos625-matching-restriction-product.yml

The module proves:

1. sdiff_matching_injective_on_bipartiteEvenEdgeSets — restriction F ↦ F \ M is injective on the finite even-edge family;

2. weighted_evenSubgraph_ennreal_matching_product —

   sum_F edgeWeightOutsideENN q M F
     <= product_{e notin M} (1 + q_e);
   

3. residualCappedEvenFixedFSum_le_lambdaProduct_mul_matchingProduct — the existing fixed-F aggregation is bounded by the local-lambda product times the direct outside-matching product.

Why

The current formalization already contains the incidence-matrix parity encoding, matching-restriction uniqueness for supported even matrices, and the fixed-F threshold aggregation. This module composes those accepted finite ingredients into the simpler endpoint proposed in PR #30.

For this particular finite algebraic bound it removes the need for a simple-cycle decomposition, residual-walk enumeration, or marked matching-cycle encoding. Those independently useful modules remain unchanged.

Validation gates

The module has direct #print axioms checks. A focused workflow:

• rejects sorry, admit, project-defined axioms/constants, and unsafe declarations;
• prepares the pinned Lean/mathlib project;
• compiles the module with -DwarningAsError=true.

The full repository Lean workflow also builds the formalization library with --wfail.

Scope boundary

This PR does not yet:

• import the module into the root aggregate or generated self-contained checkpoint;
• identify the fixed-F sum with the tagged actual attachment expectation;
• prove the analytic O(U^2 + U^4/m_0) envelope;
• prove Lemma 9.1, Proposition 9.2, or Erdos625Statement.

The audit file records the exact remaining bridges.